Nuprl Lemma : restriction-to-field
11,40
postcript
pdf
T
:Type,
R
:(
T
T
),
P
:(
T
).
(
x
,
y
:
T
. (
R
(
x
,
y
))
(
P
(
x
) &
P
(
y
)))
(
x
,
y
:
T
. (
R
|
P
(
x
,
y
))
(
R
(
x
,
y
)))
latex
Definitions
R
|
P
,
,
Type
,
x
:
A
B
(
x
)
,
P
Q
,
x
:
A
B
(
x
)
,
P
Q
,
P
Q
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
f
(
a
)
origin
T:Type, R:(T
T
), P:(T).
x, y:T. (R(x,y)) 
(P(x) & P(y))) (x, y:T. (R|P(x,y)) 
(R(x,y))) T:Type, R:(TT), P:(T).
x, y:T. (R(x,y)) (P(x) & P(y))) (x, y:T. (R|P(x,y)) (R(x,y))) B(x) Q
B(x) Q Qx:A. B(x)